eclseq($a$; $b$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr (inl $<$$a$, $b$$>$ )